#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <setjmp.h>
// Apple: #include <malloc.h>
#include <math.h>
#include <string>
#include <vector>
#include <map>
#include <algorithm>
#include <iostream>

using std::string;
using std::vector;
using std::map;
using namespace std;


int main(int argc, char* argv[]) {
  
  int N, M;

  if ( argc != 3 ) {
    cout << "Usage: muddy-gen <N> <M> " << endl;
    cout << "Where N > 2 is the number of children and M is the flag for the formulas" << endl;
    exit(1);
  }
  else {
    N = atoi(argv[1]);
    M = atoi(argv[2]);
  }
  
  cout << "-- The protocol for the muddy children" << endl <<
    "-- This file is automatically generated for " << N <<
    " children" << endl << endl;

  cout << "Agent Environment" << endl <<
    "  Obsvars:" << endl <<
    "    sayexist: boolean;" << endl << 
    "  end Obsvars" << endl << endl <<
    "  Vars:" << endl <<
    "    initial: boolean;" << endl <<
    "    total: 0.." << N << ";" << endl <<
    "  end Vars" << endl << endl <<
    "  RedStates:" << endl <<
    "  end RedStates" << endl << endl <<
    "  Actions = { exists, ask };" << endl <<
    "  Protocol:" << endl <<
    "    initial=true and total=0: {ask};" << endl <<
    "    initial=true and total>0: {exists};" << endl <<
    "    initial=false: {ask};" << endl <<
    "  end Protocol" << endl << endl <<
    "  Evolution:" << endl <<
    "    initial=false and sayexist=true if initial=true and Action=exists;" << endl <<
    "    initial=false if initial=true and Action=ask;" << endl <<
    "  end Evolution" << endl << 
    "end Agent" << endl << endl;

  
  for (int i=0; i < N; i++) {
    cout << "Agent Child" << i+1 << endl;
    cout << "  Vars:" << endl;
    cout << "    see: 0.." << (N-1) << ";" << endl;
    cout << "    mem: -1.." << (N-1) << ";" << endl;
    cout << "    othersayknow: boolean;" << endl;
    cout << "  end Vars" << endl;
    cout << "  RedStates:" << endl;
    cout << "  end RedStates" << endl;
    cout << "  Actions = { donotknow, know };" << endl;
    cout << "  Protocol:" << endl;
    cout << "    mem<see: {donotknow};" << endl;
    cout << "    mem>=see: {know};" << endl;
    cout << "  end Protocol" << endl;
  	
    cout << "  Evolution:" << endl;
    cout << "    mem = mem + 1 if Environment.Action=exists;" << endl;
    cout << "    mem = mem + 1 if Environment.Action=ask and mem<see and (othersayknow=true or (";
    
    bool first = true;
    for(int j=0; j<N; j++)
      if(i!=j) {
	if(!first)
	  cout << " and ";
	cout << "Child" << (j+1) << ".Action=donotknow";
	first = false;
      }
    cout << "));" << endl;
    cout << "    mem = mem + 1  and othersayknow=true if Environment.Action=ask and mem<see and othersayknow=false and (";
    
    first = true;
    for(int j=0; j<N; j++)
      if(i!=j) {
	if(!first)
	  cout << " or ";
	cout << "Child" << (j+1) << ".Action=know";
	first = false;
      }
    cout << ");" << endl;
    cout << "  end Evolution" << endl;

    cout << "end Agent" << endl << endl;
  }


  cout << "Evaluation" << endl;
  for ( int i=0; i < N; i++ ) {
    cout << "  muddy"<<i+1<<" if Child"<<i+1<<".see<Environment.total;" << endl;
  }
  for ( int i=0; i < N; i++ ) {
    cout << "  saysknows"<<i+1<<" if Child"<<i+1<<".see<=Child" << (i+1) <<".mem;" << endl;
  }
  cout << "end Evaluation" << endl << endl;
  
  
  cout << "InitStates" << endl;
  vector<vector<int>*> permutations;
  vector<unsigned int> heads;
  for ( int j = 0; j < ( (int)pow(2,N) ) ; j++ ) {
    unsigned int num_heads = 0;
    vector<int> *coins = new vector<int>();
     for ( int k = 0; k < N; k++ ){
       if ( j & ((int)pow(2,k))) {
	 coins->push_back(0);
       } else {
	 coins->push_back(1);
	 num_heads ++;
       }
     }
     permutations.push_back(coins);
     heads.push_back(num_heads);
  }
  cout << "    (";
  unsigned int num_permutations = (unsigned int)permutations.size();
  for(unsigned int j=0; j<num_permutations; j++) {
    vector<int> *coins = permutations[j];
    unsigned int num_heads = heads[j];
    
    if(j>0)
      cout << "     ";
    cout << "(";

    // all  children
    for (int k=1; k<=N; k++) {
      cout << " Child"<<k<<".see=" << heads[j]-(*coins)[k-1] << " and "; 
    }

    cout << "Environment.total=" << heads[j] << ")";
     if ( j != num_permutations-1 ) {
       cout << " or " << endl;
     }
  }
  cout << ") and" << endl;

  for ( int k=1; k<=N; k++ ) {
    cout << "    Child" << k << ".othersayknow=false and Child" << k << ".mem=-1 and" << endl;
  }
  cout << "    Environment.sayexist=false and Environment.initial=true;" << endl;

  cout << "end InitStates" << endl << endl;

  cout << "Groups" << endl;
  cout << "end Groups" << endl << endl;

  cout << "Fairness" << endl;
  cout << "end Fairness" << endl << endl;

  cout << "Formulae"<< endl;
  
  /*for(unsigned int j=1; j<=N; j++) {
    cout << "  AG((saysknows" << j << " -> (K(Child" << j << ", muddy" << j << ") or K(Child"
	 << j << ", !muddy" << j << "))) and " << endl;
    cout << "    ((K(Child" << j << ", muddy" << j << ") or K(Child"
	 << j << ", !muddy" << j << ")) -> saysknows" << j << "))";
    if(j<N)
      cout << " and " << endl;
    else
      cout << ";" << endl;
      }*/
  if(M==0)
    cout << "  AG((K(Child1, muddy1) or K(Child1, !muddy1)) -> saysknows1);" << endl;
  else if(M==1) {
    for(int i=1; i<=N; i++)
      cout << "  AG((K(Child" << i << ", muddy" << i << ") or K(Child" << i << ", !muddy" << i << ")) -> saysknows" << i << ");" << endl;

  } else if(M==2) {
    cout << "  AG((K(Child1, muddy1) or K(Child1, !muddy1)) -> saysknows1);" << endl;
    cout << "  AG((K(Child" << N << ", muddy" << N << ") or K(Child" << N << ", !muddy" << N << ")) -> saysknows" << N << ");" << endl;
  } else {
    for(int i=1; i<=N; i++) {
      cout << "  AG(saysknows" << i << " -> (K(Child" << i << ", muddy" << i << ") or K(Child" << i << ", !muddy" << i << ")));" << endl;
      cout << "  AG((K(Child" << i << ", muddy" << i << ") or K(Child" << i << ", !muddy" << i << ")) -> saysknows" << i << ");" << endl;
    }
  }
  cout << "end Formulae" << endl;

}

